Matches in value-assignements (V): {{numOfValueMatches}}
Matches in edge-description: {{numOfDescriptionMatches}}
Rank |
Scope |
|||
-V- |
{{line.bestrank}}
|
{{line.desc}}
|
| Precondition (initial variable assignment): |
|
{{precondition}} |
| {{fault.rank}}. | {{fault.score}} | Details: | ||||
Current values:
|
||||||
1 | extern void __VERIFIER_error() __attribute__ ((__noreturn__)); |
2 | |
3 | typedef long unsigned int size_t; |
4 | typedef int wchar_t; |
5 | |
6 | union wait |
7 | { |
8 | int w_status; |
9 | struct |
10 | { |
11 | unsigned int __w_termsig:7; |
12 | unsigned int __w_coredump:1; |
13 | unsigned int __w_retcode:8; |
14 | unsigned int:16; |
15 | } __wait_terminated; |
16 | struct |
17 | { |
18 | unsigned int __w_stopval:8; |
19 | unsigned int __w_stopsig:8; |
20 | unsigned int:16; |
21 | } __wait_stopped; |
22 | }; |
23 | typedef union |
24 | { |
25 | union wait *__uptr; |
26 | int *__iptr; |
27 | } __WAIT_STATUS __attribute__ ((__transparent_union__)); |
28 | |
29 | typedef struct |
30 | { |
31 | int quot; |
32 | int rem; |
33 | } div_t; |
34 | typedef struct |
35 | { |
36 | long int quot; |
37 | long int rem; |
38 | } ldiv_t; |
39 | |
40 | |
41 | __extension__ typedef struct |
42 | { |
43 | long long int quot; |
44 | long long int rem; |
45 | } lldiv_t; |
46 | |
47 | extern size_t __ctype_get_mb_cur_max (void) __attribute__ ((__nothrow__ , __leaf__)) ; |
48 | |
49 | extern double atof (__const char *__nptr) |
50 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1))) ; |
51 | extern int atoi (__const char *__nptr) |
52 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1))) ; |
53 | extern long int atol (__const char *__nptr) |
54 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1))) ; |
55 | |
56 | |
57 | __extension__ extern long long int atoll (__const char *__nptr) |
58 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1))) ; |
59 | |
60 | |
61 | extern double strtod (__const char *__restrict __nptr, |
62 | char **__restrict __endptr) |
63 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ; |
64 | |
65 | |
66 | extern float strtof (__const char *__restrict __nptr, |
67 | char **__restrict __endptr) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ; |
68 | extern long double strtold (__const char *__restrict __nptr, |
69 | char **__restrict __endptr) |
70 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ; |
71 | |
72 | |
73 | extern long int strtol (__const char *__restrict __nptr, |
74 | char **__restrict __endptr, int __base) |
75 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ; |
76 | extern unsigned long int strtoul (__const char *__restrict __nptr, |
77 | char **__restrict __endptr, int __base) |
78 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ; |
79 | |
80 | __extension__ |
81 | extern long long int strtoq (__const char *__restrict __nptr, |
82 | char **__restrict __endptr, int __base) |
83 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ; |
84 | __extension__ |
85 | extern unsigned long long int strtouq (__const char *__restrict __nptr, |
86 | char **__restrict __endptr, int __base) |
87 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ; |
88 | |
89 | __extension__ |
90 | extern long long int strtoll (__const char *__restrict __nptr, |
91 | char **__restrict __endptr, int __base) |
92 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ; |
93 | __extension__ |
94 | extern unsigned long long int strtoull (__const char *__restrict __nptr, |
95 | char **__restrict __endptr, int __base) |
96 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ; |
97 | |
98 | extern char *l64a (long int __n) __attribute__ ((__nothrow__ , __leaf__)) ; |
99 | extern long int a64l (__const char *__s) |
100 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1))) ; |
101 | |
102 | typedef unsigned char __u_char; |
103 | typedef unsigned short int __u_short; |
104 | typedef unsigned int __u_int; |
105 | typedef unsigned long int __u_long; |
106 | typedef signed char __int8_t; |
107 | typedef unsigned char __uint8_t; |
108 | typedef signed short int __int16_t; |
109 | typedef unsigned short int __uint16_t; |
110 | typedef signed int __int32_t; |
111 | typedef unsigned int __uint32_t; |
112 | typedef signed long int __int64_t; |
113 | typedef unsigned long int __uint64_t; |
114 | typedef long int __quad_t; |
115 | typedef unsigned long int __u_quad_t; |
116 | typedef unsigned long int __dev_t; |
117 | typedef unsigned int __uid_t; |
118 | typedef unsigned int __gid_t; |
119 | typedef unsigned long int __ino_t; |
120 | typedef unsigned long int __ino64_t; |
121 | typedef unsigned int __mode_t; |
122 | typedef unsigned long int __nlink_t; |
123 | typedef long int __off_t; |
124 | typedef long int __off64_t; |
125 | typedef int __pid_t; |
126 | typedef struct { int __val[2]; } __fsid_t; |
127 | typedef long int __clock_t; |
128 | typedef unsigned long int __rlim_t; |
129 | typedef unsigned long int __rlim64_t; |
130 | typedef unsigned int __id_t; |
131 | typedef long int __time_t; |
132 | typedef unsigned int __useconds_t; |
133 | typedef long int __suseconds_t; |
134 | typedef int __daddr_t; |
135 | typedef long int __swblk_t; |
136 | typedef int __key_t; |
137 | typedef int __clockid_t; |
138 | typedef void * __timer_t; |
139 | typedef long int __blksize_t; |
140 | typedef long int __blkcnt_t; |
141 | typedef long int __blkcnt64_t; |
142 | typedef unsigned long int __fsblkcnt_t; |
143 | typedef unsigned long int __fsblkcnt64_t; |
144 | typedef unsigned long int __fsfilcnt_t; |
145 | typedef unsigned long int __fsfilcnt64_t; |
146 | typedef long int __ssize_t; |
147 | typedef __off64_t __loff_t; |
148 | typedef __quad_t *__qaddr_t; |
149 | typedef char *__caddr_t; |
150 | typedef long int __intptr_t; |
151 | typedef unsigned int __socklen_t; |
152 | typedef __u_char u_char; |
153 | typedef __u_short u_short; |
154 | typedef __u_int u_int; |
155 | typedef __u_long u_long; |
156 | typedef __quad_t quad_t; |
157 | typedef __u_quad_t u_quad_t; |
158 | typedef __fsid_t fsid_t; |
159 | typedef __loff_t loff_t; |
160 | typedef __ino_t ino_t; |
161 | typedef __dev_t dev_t; |
162 | typedef __gid_t gid_t; |
163 | typedef __mode_t mode_t; |
164 | typedef __nlink_t nlink_t; |
165 | typedef __uid_t uid_t; |
166 | typedef __off_t off_t; |
167 | typedef __pid_t pid_t; |
168 | typedef __id_t id_t; |
169 | typedef __ssize_t ssize_t; |
170 | typedef __daddr_t daddr_t; |
171 | typedef __caddr_t caddr_t; |
172 | typedef __key_t key_t; |
173 | |
174 | typedef __clock_t clock_t; |
175 | |
176 | |
177 | |
178 | typedef __time_t time_t; |
179 | |
180 | |
181 | typedef __clockid_t clockid_t; |
182 | typedef __timer_t timer_t; |
183 | typedef unsigned long int ulong; |
184 | typedef unsigned short int ushort; |
185 | typedef unsigned int uint; |
186 | typedef int int8_t __attribute__ ((__mode__ (__QI__))); |
187 | typedef int int16_t __attribute__ ((__mode__ (__HI__))); |
188 | typedef int int32_t __attribute__ ((__mode__ (__SI__))); |
189 | typedef int int64_t __attribute__ ((__mode__ (__DI__))); |
190 | typedef unsigned int u_int8_t __attribute__ ((__mode__ (__QI__))); |
191 | typedef unsigned int u_int16_t __attribute__ ((__mode__ (__HI__))); |
192 | typedef unsigned int u_int32_t __attribute__ ((__mode__ (__SI__))); |
193 | typedef unsigned int u_int64_t __attribute__ ((__mode__ (__DI__))); |
194 | typedef int register_t __attribute__ ((__mode__ (__word__))); |
195 | typedef int __sig_atomic_t; |
196 | typedef struct |
197 | { |
198 | unsigned long int __val[(1024 / (8 * sizeof (unsigned long int)))]; |
199 | } __sigset_t; |
200 | typedef __sigset_t sigset_t; |
201 | struct timespec |
202 | { |
203 | __time_t tv_sec; |
204 | long int tv_nsec; |
205 | }; |
206 | struct timeval |
207 | { |
208 | __time_t tv_sec; |
209 | __suseconds_t tv_usec; |
210 | }; |
211 | typedef __suseconds_t suseconds_t; |
212 | typedef long int __fd_mask; |
213 | typedef struct |
214 | { |
215 | __fd_mask __fds_bits[1024 / (8 * (int) sizeof (__fd_mask))]; |
216 | } fd_set; |
217 | typedef __fd_mask fd_mask; |
218 | |
219 | extern int select (int __nfds, fd_set *__restrict __readfds, |
220 | fd_set *__restrict __writefds, |
221 | fd_set *__restrict __exceptfds, |
222 | struct timeval *__restrict __timeout); |
223 | extern int pselect (int __nfds, fd_set *__restrict __readfds, |
224 | fd_set *__restrict __writefds, |
225 | fd_set *__restrict __exceptfds, |
226 | const struct timespec *__restrict __timeout, |
227 | const __sigset_t *__restrict __sigmask); |
228 | |
229 | |
230 | __extension__ |
231 | extern unsigned int gnu_dev_major (unsigned long long int __dev) |
232 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)); |
233 | __extension__ |
234 | extern unsigned int gnu_dev_minor (unsigned long long int __dev) |
235 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)); |
236 | __extension__ |
237 | extern unsigned long long int gnu_dev_makedev (unsigned int __major, |
238 | unsigned int __minor) |
239 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)); |
240 | |
241 | typedef __blksize_t blksize_t; |
242 | typedef __blkcnt_t blkcnt_t; |
243 | typedef __fsblkcnt_t fsblkcnt_t; |
244 | |
245 | |
246 | typedef __fsfilcnt_t fsfilcnt_t; |
247 | typedef unsigned long int pthread_t; |
248 | typedef union |
249 | { |
250 | char __size[56]; |
251 | long int __align; |
252 | } pthread_attr_t; |
253 | typedef struct __pthread_internal_list |
254 | { |
255 | struct __pthread_internal_list *__prev; |
256 | struct __pthread_internal_list *__next; |
257 | } __pthread_list_t; |
258 | typedef union |
259 | { |
260 | struct __pthread_mutex_s |
261 | { |
262 | int __lock; |
263 | unsigned int __count; |
264 | int __owner; |
265 | unsigned int __nusers; |
266 | int __kind; |
267 | int __spins; |
268 | __pthread_list_t __list; |
269 | } __data; |
270 | char __size[40]; |
271 | long int __align; |
272 | } pthread_mutex_t; |
273 | typedef union |
274 | { |
275 | char __size[4]; |
276 | int __align; |
277 | } pthread_mutexattr_t; |
278 | typedef union |
279 | { |
280 | struct |
281 | { |
282 | int __lock; |
283 | unsigned int __futex; |
284 | __extension__ unsigned long long int __total_seq; |
285 | __extension__ unsigned long long int __wakeup_seq; |
286 | __extension__ unsigned long long int __woken_seq; |
287 | void *__mutex; |
288 | unsigned int __nwaiters; |
289 | unsigned int __broadcast_seq; |
290 | } __data; |
291 | char __size[48]; |
292 | __extension__ long long int __align; |
293 | } pthread_cond_t; |
294 | typedef union |
295 | { |
296 | char __size[4]; |
297 | int __align; |
298 | } pthread_condattr_t; |
299 | typedef unsigned int pthread_key_t; |
300 | typedef int pthread_once_t; |
301 | typedef union |
302 | { |
303 | struct |
304 | { |
305 | int __lock; |
306 | unsigned int __nr_readers; |
307 | unsigned int __readers_wakeup; |
308 | unsigned int __writer_wakeup; |
309 | unsigned int __nr_readers_queued; |
310 | unsigned int __nr_writers_queued; |
311 | int __writer; |
312 | int __shared; |
313 | unsigned long int __pad1; |
314 | unsigned long int __pad2; |
315 | unsigned int __flags; |
316 | } __data; |
317 | char __size[56]; |
318 | long int __align; |
319 | } pthread_rwlock_t; |
320 | typedef union |
321 | { |
322 | char __size[8]; |
323 | long int __align; |
324 | } pthread_rwlockattr_t; |
325 | typedef volatile int pthread_spinlock_t; |
326 | typedef union |
327 | { |
328 | char __size[32]; |
329 | long int __align; |
330 | } pthread_barrier_t; |
331 | typedef union |
332 | { |
333 | char __size[4]; |
334 | int __align; |
335 | } pthread_barrierattr_t; |
336 | |
337 | extern long int random (void) __attribute__ ((__nothrow__ , __leaf__)); |
338 | extern void srandom (unsigned int __seed) __attribute__ ((__nothrow__ , __leaf__)); |
339 | extern char *initstate (unsigned int __seed, char *__statebuf, |
340 | size_t __statelen) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2))); |
341 | |
342 | |
343 | extern char *setstate (char *__statebuf) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); |
344 | |
345 | |
346 | |
347 | |
348 | |
349 | |
350 | |
351 | struct random_data |
352 | { |
353 | int32_t *fptr; |
354 | int32_t *rptr; |
355 | int32_t *state; |
356 | int rand_type; |
357 | int rand_deg; |
358 | int rand_sep; |
359 | int32_t *end_ptr; |
360 | }; |
361 | |
362 | extern int random_r (struct random_data *__restrict __buf, |
363 | int32_t *__restrict __result) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); |
364 | |
365 | extern int srandom_r (unsigned int __seed, struct random_data *__buf) |
366 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2))); |
367 | |
368 | extern int initstate_r (unsigned int __seed, char *__restrict __statebuf, |
369 | size_t __statelen, |
370 | struct random_data *__restrict __buf) |
371 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2, 4))); |
372 | |
373 | extern int setstate_r (char *__restrict __statebuf, |
374 | struct random_data *__restrict __buf) |
375 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); |
376 | |
377 | |
378 | |
379 | |
380 | |
381 | |
382 | extern int rand (void) __attribute__ ((__nothrow__ , __leaf__)); |
383 | |
384 | extern void srand (unsigned int __seed) __attribute__ ((__nothrow__ , __leaf__)); |
385 | |
386 | |
387 | |
388 | |
389 | extern int rand_r (unsigned int *__seed) __attribute__ ((__nothrow__ , __leaf__)); |
390 | |
391 | |
392 | |
393 | |
394 | |
395 | |
396 | |
397 | extern double drand48 (void) __attribute__ ((__nothrow__ , __leaf__)); |
398 | extern double erand48 (unsigned short int __xsubi[3]) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); |
399 | |
400 | |
401 | extern long int lrand48 (void) __attribute__ ((__nothrow__ , __leaf__)); |
402 | extern long int nrand48 (unsigned short int __xsubi[3]) |
403 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); |
404 | |
405 | |
406 | extern long int mrand48 (void) __attribute__ ((__nothrow__ , __leaf__)); |
407 | extern long int jrand48 (unsigned short int __xsubi[3]) |
408 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); |
409 | |
410 | |
411 | extern void srand48 (long int __seedval) __attribute__ ((__nothrow__ , __leaf__)); |
412 | extern unsigned short int *seed48 (unsigned short int __seed16v[3]) |
413 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); |
414 | extern void lcong48 (unsigned short int __param[7]) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); |
415 | |
416 | |
417 | |
418 | |
419 | |
420 | struct drand48_data |
421 | { |
422 | unsigned short int __x[3]; |
423 | unsigned short int __old_x[3]; |
424 | unsigned short int __c; |
425 | unsigned short int __init; |
426 | unsigned long long int __a; |
427 | }; |
428 | |
429 | |
430 | extern int drand48_r (struct drand48_data *__restrict __buffer, |
431 | double *__restrict __result) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); |
432 | extern int erand48_r (unsigned short int __xsubi[3], |
433 | struct drand48_data *__restrict __buffer, |
434 | double *__restrict __result) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); |
435 | |
436 | |
437 | extern int lrand48_r (struct drand48_data *__restrict __buffer, |
438 | long int *__restrict __result) |
439 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); |
440 | extern int nrand48_r (unsigned short int __xsubi[3], |
441 | struct drand48_data *__restrict __buffer, |
442 | long int *__restrict __result) |
443 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); |
444 | |
445 | |
446 | extern int mrand48_r (struct drand48_data *__restrict __buffer, |
447 | long int *__restrict __result) |
448 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); |
449 | extern int jrand48_r (unsigned short int __xsubi[3], |
450 | struct drand48_data *__restrict __buffer, |
451 | long int *__restrict __result) |
452 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); |
453 | |
454 | |
455 | extern int srand48_r (long int __seedval, struct drand48_data *__buffer) |
456 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2))); |
457 | |
458 | extern int seed48_r (unsigned short int __seed16v[3], |
459 | struct drand48_data *__buffer) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); |
460 | |
461 | extern int lcong48_r (unsigned short int __param[7], |
462 | struct drand48_data *__buffer) |
463 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2))); |
464 | |
465 | |
466 | |
467 | |
468 | |
469 | |
470 | |
471 | |
472 | |
473 | extern void *malloc (size_t __size) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__malloc__)) ; |
474 | |
475 | extern void *calloc (size_t __nmemb, size_t __size) |
476 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__malloc__)) ; |
477 | |
478 | |
479 | |
480 | |
481 | |
482 | |
483 | |
484 | |
485 | |
486 | |
487 | extern void *realloc (void *__ptr, size_t __size) |
488 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__warn_unused_result__)); |
489 | |
490 | extern void free (void *__ptr) __attribute__ ((__nothrow__ , __leaf__)); |
491 | |
492 | |
493 | |
494 | |
495 | extern void cfree (void *__ptr) __attribute__ ((__nothrow__ , __leaf__)); |
496 | |
497 | extern void *alloca (size_t __size) __attribute__ ((__nothrow__ , __leaf__)); |
498 | |
499 | |
500 | |
501 | |
502 | |
503 | |
504 | |
505 | extern void *valloc (size_t __size) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__malloc__)) ; |
506 | |
507 | |
508 | |
509 | |
510 | extern int posix_memalign (void **__memptr, size_t __alignment, size_t __size) |
511 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ; |
512 | |
513 | |
514 | |
515 | |
516 | extern void abort (void) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__)); |
517 | |
518 | |
519 | |
520 | extern int atexit (void (*__func) (void)) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); |
521 | |
522 | extern int on_exit (void (*__func) (int __status, void *__arg), void *__arg) |
523 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); |
524 | |
525 | extern void exit (int __status) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__)); |
526 | |
527 | |
528 | extern void _Exit (int __status) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__)); |
529 | |
530 | |
531 | extern char *getenv (__const char *__name) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ; |
532 | |
533 | extern char *__secure_getenv (__const char *__name) |
534 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ; |
535 | extern int putenv (char *__string) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); |
536 | extern int setenv (__const char *__name, __const char *__value, int __replace) |
537 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2))); |
538 | extern int unsetenv (__const char *__name) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); |
539 | extern int clearenv (void) __attribute__ ((__nothrow__ , __leaf__)); |
540 | extern char *mktemp (char *__template) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ; |
541 | extern int mkstemp (char *__template) __attribute__ ((__nonnull__ (1))) ; |
542 | extern int mkstemps (char *__template, int __suffixlen) __attribute__ ((__nonnull__ (1))) ; |
543 | extern char *mkdtemp (char *__template) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ; |
544 | |
545 | extern int system (__const char *__command) ; |
546 | |
547 | extern char *realpath (__const char *__restrict __name, |
548 | char *__restrict __resolved) __attribute__ ((__nothrow__ , __leaf__)) ; |
549 | typedef int (*__compar_fn_t) (__const void *, __const void *); |
550 | |
551 | extern void *bsearch (__const void *__key, __const void *__base, |
552 | size_t __nmemb, size_t __size, __compar_fn_t __compar) |
553 | __attribute__ ((__nonnull__ (1, 2, 5))) ; |
554 | extern void qsort (void *__base, size_t __nmemb, size_t __size, |
555 | __compar_fn_t __compar) __attribute__ ((__nonnull__ (1, 4))); |
556 | extern int abs (int __x) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)) ; |
557 | extern long int labs (long int __x) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)) ; |
558 | |
559 | __extension__ extern long long int llabs (long long int __x) |
560 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)) ; |
561 | |
562 | extern div_t div (int __numer, int __denom) |
563 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)) ; |
564 | extern ldiv_t ldiv (long int __numer, long int __denom) |
565 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)) ; |
566 | |
567 | |
568 | __extension__ extern lldiv_t lldiv (long long int __numer, |
569 | long long int __denom) |
570 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)) ; |
571 | |
572 | extern char *ecvt (double __value, int __ndigit, int *__restrict __decpt, |
573 | int *__restrict __sign) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4))) ; |
574 | extern char *fcvt (double __value, int __ndigit, int *__restrict __decpt, |
575 | int *__restrict __sign) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4))) ; |
576 | extern char *gcvt (double __value, int __ndigit, char *__buf) |
577 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3))) ; |
578 | extern char *qecvt (long double __value, int __ndigit, |
579 | int *__restrict __decpt, int *__restrict __sign) |
580 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4))) ; |
581 | extern char *qfcvt (long double __value, int __ndigit, |
582 | int *__restrict __decpt, int *__restrict __sign) |
583 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4))) ; |
584 | extern char *qgcvt (long double __value, int __ndigit, char *__buf) |
585 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3))) ; |
586 | extern int ecvt_r (double __value, int __ndigit, int *__restrict __decpt, |
587 | int *__restrict __sign, char *__restrict __buf, |
588 | size_t __len) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4, 5))); |
589 | extern int fcvt_r (double __value, int __ndigit, int *__restrict __decpt, |
590 | int *__restrict __sign, char *__restrict __buf, |
591 | size_t __len) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4, 5))); |
592 | extern int qecvt_r (long double __value, int __ndigit, |
593 | int *__restrict __decpt, int *__restrict __sign, |
594 | char *__restrict __buf, size_t __len) |
595 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4, 5))); |
596 | extern int qfcvt_r (long double __value, int __ndigit, |
597 | int *__restrict __decpt, int *__restrict __sign, |
598 | char *__restrict __buf, size_t __len) |
599 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4, 5))); |
600 | |
601 | extern int mblen (__const char *__s, size_t __n) __attribute__ ((__nothrow__ , __leaf__)) ; |
602 | extern int mbtowc (wchar_t *__restrict __pwc, |
603 | __const char *__restrict __s, size_t __n) __attribute__ ((__nothrow__ , __leaf__)) ; |
604 | extern int wctomb (char *__s, wchar_t __wchar) __attribute__ ((__nothrow__ , __leaf__)) ; |
605 | extern size_t mbstowcs (wchar_t *__restrict __pwcs, |
606 | __const char *__restrict __s, size_t __n) __attribute__ ((__nothrow__ , __leaf__)); |
607 | extern size_t wcstombs (char *__restrict __s, |
608 | __const wchar_t *__restrict __pwcs, size_t __n) |
609 | __attribute__ ((__nothrow__ , __leaf__)); |
610 | |
611 | extern int rpmatch (__const char *__response) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ; |
612 | extern int getsubopt (char **__restrict __optionp, |
613 | char *__const *__restrict __tokens, |
614 | char **__restrict __valuep) |
615 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2, 3))) ; |
616 | extern int getloadavg (double __loadavg[], int __nelem) |
617 | __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); |
618 | |
619 | extern int __VERIFIER_nondet_int(void); |
620 | static void fail(void) { |
621 | ERROR: __VERIFIER_error(); |
622 | } |
623 | struct node { |
624 | struct node *next; |
625 | int value; |
626 | }; |
627 | struct list { |
628 | struct node *slist; |
629 | struct list *next; |
630 | }; |
631 | static void merge_single_node(struct node ***dst, |
632 | struct node **data) |
633 | { |
634 | struct node *node = *data; |
635 | *data = node->next; |
636 | node->next = ((void *)0); |
637 | **dst = node; |
638 | *dst = &node->next; |
639 | } |
640 | static void merge_pair(struct node **dst, |
641 | struct node *sub1, |
642 | struct node *sub2) |
643 | { |
644 | while (sub1 || sub2) { |
645 | if (!sub2 || (sub1 && sub1->value < sub2->value)) |
646 | merge_single_node(&dst, &sub1); |
647 | else |
648 | merge_single_node(&dst, &sub2); |
649 | } |
650 | } |
651 | static struct list* seq_sort_core(struct list *data) |
652 | { |
653 | struct list *dst = ((void *)0); |
654 | while (data) { |
655 | struct list *next = data->next; |
656 | if (!next) { |
657 | data->next = dst; |
658 | dst = data; |
659 | break; |
660 | } |
661 | merge_pair(&data->slist, data->slist, next->slist); |
662 | data->next = dst; |
663 | dst = data; |
664 | data = next->next; |
665 | free(next); |
666 | } |
667 | return dst; |
668 | } |
669 | static void inspect_before(struct list *shape) |
670 | { |
671 | do { if (!(shape)) fail(); } while (0); |
672 | for (; shape->next; shape = shape->next) { |
673 | do { if (!(shape)) fail(); } while (0); |
674 | do { if (!(shape->next)) fail(); } while (0); |
675 | do { if (!(shape->slist)) fail(); } while (0); |
676 | do { if (!(shape->slist->next == ((void *)0))) fail(); } while (0); |
677 | } |
678 | do { if (!(shape)) fail(); } while (0); |
679 | do { if (!(shape->next == ((void *)0))) fail(); } while (0); |
680 | do { if (!(shape->slist)) fail(); } while (0); |
681 | do { if (!(shape->slist->next == ((void *)0))) fail(); } while (0); |
682 | } |
683 | static void inspect_after(struct list *shape) |
684 | { |
685 | do { if (!(shape)) fail(); } while (0); |
686 | do { if (!(shape->next == ((void *)0))) fail(); } while (0); |
687 | do { if (!(shape->slist != ((void *)0))) fail(); } while (0); |
688 | struct node *pos; |
689 | for (pos = shape->slist; pos->next; pos = pos->next); |
690 | do { if (!(!pos->next)) fail(); } while (0); |
691 | } |
692 | int main() |
693 | { |
694 | struct list *data = ((void *)0); |
695 | while (__VERIFIER_nondet_int()) { |
696 | struct node *node = malloc(sizeof *node); |
697 | if (!node) |
698 | abort(); |
699 | node->next = ((void *)0); |
700 | node->value = __VERIFIER_nondet_int(); |
701 | struct list *item = malloc(sizeof *item); |
702 | if (!item) |
703 | abort(); |
704 | item->slist = node; |
705 | item->next = data; |
706 | data = item; |
707 | } |
708 | if (!data) |
709 | return 0; |
710 | inspect_before(data); |
711 | while (data->next) |
712 | data = seq_sort_core(data); |
713 | inspect_after(data); |
714 | struct node *node = data->slist; |
715 | free(data); |
716 | while (node) { |
717 | struct node *snext = node->next; |
718 | free(node); |
719 | node = snext; |
720 | } |
721 | return 0; |
722 | } |
| Date | Time | Level | Component | Message |
|---|---|---|---|---|
| 2025-08-28 | 06:59:43:617 | INFO | CPAMain.detectFrontendLanguageIfNecessary | Language C detected and set for analysis |
| 2025-08-28 | 06:59:43:697 | INFO | CPAchecker.run | CPAchecker 4.0 / terminationAnalysis (OpenJDK 64-Bit Server VM 17.0.15) started |
| 2025-08-28 | 06:59:43:715 | INFO | CPAchecker.parse | Parsing CFA from file(s) "Benchmarks/TermCOMP/C/SV-COMP_Mixed_Categories/merge_sort_true-unreach-call/merge_sort_true-unreach-call.c" |
| 2025-08-28 | 06:59:44:790 | INFO | CFACreationUtils.addEdgeToCFA | line 671: Dead code detected: |
| 2025-08-28 | 06:59:44:793 | INFO | CFACreationUtils.addEdgeToCFA | line 673: Dead code detected: |
| 2025-08-28 | 06:59:44:795 | INFO | CFACreationUtils.addEdgeToCFA | line 674: Dead code detected: |
| 2025-08-28 | 06:59:44:796 | INFO | CFACreationUtils.addEdgeToCFA | line 675: Dead code detected: |
| 2025-08-28 | 06:59:44:797 | INFO | CFACreationUtils.addEdgeToCFA | line 676: Dead code detected: |
| 2025-08-28 | 06:59:44:799 | INFO | CFACreationUtils.addEdgeToCFA | line 678: Dead code detected: |
| 2025-08-28 | 06:59:44:800 | INFO | CFACreationUtils.addEdgeToCFA | line 679: Dead code detected: |
| 2025-08-28 | 06:59:44:801 | INFO | CFACreationUtils.addEdgeToCFA | line 680: Dead code detected: |
| 2025-08-28 | 06:59:44:802 | INFO | CFACreationUtils.addEdgeToCFA | line 681: Dead code detected: |
| 2025-08-28 | 06:59:44:805 | INFO | CFACreationUtils.addEdgeToCFA | line 685: Dead code detected: |
| 2025-08-28 | 06:59:44:807 | INFO | CFACreationUtils.addEdgeToCFA | line 686: Dead code detected: |
| 2025-08-28 | 06:59:44:808 | INFO | CFACreationUtils.addEdgeToCFA | line 687: Dead code detected: |
| 2025-08-28 | 06:59:44:811 | INFO | CFACreationUtils.addEdgeToCFA | line 690: Dead code detected: |
| 2025-08-28 | 06:59:45:139 | INFO | CoreComponentsFactory.createAlgorithm | Using Restarting Algorithm |
| 2025-08-28 | 06:59:45:161 | WARNING | CPAchecker.printConfigurationWarnings | The following configuration options were specified but are not used: cpa.arg.lateMerge counterexample.export.exportWitness |
| 2025-08-28 | 06:59:45:162 | INFO | CPAchecker.runAlgorithm | Starting analysis ... |
| 2025-08-28 | 06:59:45:172 | INFO | RestartAlgorithm.run | Loading analysis 1 from file /cpachecker/config/components/combinations-parallel-termination.properties ... |
| 2025-08-28 | 06:59:45:240 | INFO | Analysis /cpachecker/config/components/combinations-parallel-termination.properties Parallel analysis 1 ResourceLimitChecker.fromConfiguration | Using the following resource limits: Thread CPU-time limit of 300s |
| 2025-08-28 | 06:59:45:635 | INFO | Analysis /cpachecker/config/components/combinations-parallel-termination.properties Parallel analysis 1 PredicateCPA PredicateCPA.<init> | Using predicate analysis with MathSAT5 version 5.6.10 (9293adc746be) (May 31 2023 12:38:06, gmp 6.2.0, gcc 7.5.0, 64-bit, reentrant) and JFactory 1.21. |
| 2025-08-28 | 06:59:46:037 | INFO | Analysis /cpachecker/config/components/combinations-parallel-termination.properties Parallel analysis 1 PredicateCPA PredicateCPARefiner.<init> | Using refinement for predicate analysis with PredicateAbstractionRefinementStrategy strategy. |
| 2025-08-28 | 06:59:46:049 | WARNING | CPAs.retrieveCPAOrFail | Warning: Skipping one analysis because the configuration file /cpachecker/config/components/combinations-parallel-termination.properties is invalid (TerminationAlgorithm needs a TerminationCPA) |
| 2025-08-28 | 06:59:46:052 | INFO | RestartAlgorithm.run | Loading analysis 1 from file /cpachecker/config/components/termination-recursion.properties ... |
| 2025-08-28 | 06:59:46:062 | INFO | NestingAlgorithm.checkConfigs | Mismatch of configuration options when loading from '/cpachecker/config/components/termination-recursion.properties': 'termination.config' has two values 'terminationAnalysis.properties' and 'termination-recursion.properties'. Using 'termination-recursion.properties'. |
| 2025-08-28 | 06:59:46:143 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties PredicateCPA FormulaManagerView.<init> | Using unsound approximation of ints with unbounded integers and floats with rationals for encoding program semantics. |
| 2025-08-28 | 06:59:46:148 | INFO | Analysis /cpachecker/config/components/termination-recursion.properties PredicateCPA PredicateCPA.<init> | Using predicate analysis with MathSAT5 version 5.6.10 (9293adc746be) (May 31 2023 12:38:06, gmp 6.2.0, gcc 7.5.0, 64-bit, reentrant) and JFactory 1.21. |
| 2025-08-28 | 06:59:46:382 | INFO | Analysis /cpachecker/config/components/termination-recursion.properties PredicateCPA PredicateCPARefiner.<init> | Using refinement for predicate analysis with PredicateAbstractionRefinementStrategy strategy. |
| 2025-08-28 | 06:59:46:453 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties FormulaManagerView.<init> | Using unsound approximation of ints with unbounded integers and floats with rationals for encoding program semantics. |
| 2025-08-28 | 06:59:46:487 | INFO | RestartAlgorithm.run | Starting analysis 1 ... |
| 2025-08-28 | 06:59:46:488 | INFO | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.run0 | Starting termination algorithm. |
| 2025-08-28 | 07:00:04:372 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties InequalityConverter.convert | Warning: Could not extract lasso (Loop with heads [N181] incoming: [line 711: N180 -{while}-> N181] outgoing: [line 711: N181 -{[(data->next) == 0]}-> N183] nodes: [N181, N182, N184] ). (Unknown sort in equality) |
| 2025-08-28 | 07:00:04:381 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-28 | 07:01:40:860 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties InequalityConverter.convert | Warning: Could not extract lasso (Loop with heads [N142] incoming: [line 689: N141 -{pos = shape->slist;}-> N142] outgoing: [line 689: N142 -{[(pos->next) == 0]}-> N145] nodes: [N142, N143, N144] ). (Unknown sort in equality) |
| 2025-08-28 | 07:01:40:863 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-28 | 07:01:41:419 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties InequalityConverter.convert | Warning: Could not extract lasso (Loop with heads [N188] incoming: [line 716: N187 -{while}-> N188] outgoing: [line 716: N188 -{[node__1 == 0]}-> N190] nodes: [N188, N189, N191, N192, N193] ). (Unknown sort in equality) |
| 2025-08-28 | 07:01:41:420 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-28 | 07:01:54:913 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties InequalityConverter.convert | Warning: Could not extract lasso (Loop with heads [N31] incoming: [line 654: N30 -{while}-> N31] outgoing: [line 654: N31 -{[data == 0]}-> N33, line 656: N34 -{[next == 0]}-> N36] nodes: [N31, N32, N34, N35, N40, N41, N42, N43, N44] ). (Unknown sort in equality) |
| 2025-08-28 | 07:01:54:914 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-28 | 07:02:08:202 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties InequalityConverter.convert | Warning: Could not extract lasso (Loop with heads [N31] incoming: [line 654: N30 -{while}-> N31] outgoing: [line 654: N31 -{[data == 0]}-> N33, line 656: N34 -{[next == 0]}-> N36] nodes: [N31, N32, N34, N35, N40, N41, N42, N43, N44] ). (Unknown sort in equality) |
| 2025-08-28 | 07:02:08:203 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-28 | 07:02:21:452 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties InequalityConverter.convert | Warning: Could not extract lasso (Loop with heads [N31] incoming: [line 654: N30 -{while}-> N31] outgoing: [line 654: N31 -{[data == 0]}-> N33, line 656: N34 -{[next == 0]}-> N36] nodes: [N31, N32, N34, N35, N40, N41, N42, N43, N44] ). (Unknown sort in equality) |
| 2025-08-28 | 07:02:21:453 | WARNING | Analysis /cpachecker/config/components/termination-recursion.properties TerminationAlgorithm.proveLoopTermination | Could not synthesize a termination or non-termination argument. |
| 2025-08-28 | 07:02:21:655 | SEVERE | RefinementFailedException.forInterpolationFailureInSolver | Error: Refinement failed: Interpolation failed in solver MATHSAT5 with message 'can't build ie-local interpolant'. |
| Statistics Name | Statistics Value | Additional Value |
|---|---|---|
| Restart Algorithm statistics | ||
| Number of algorithms provided | 2 | |
| Number of algorithms used | 1 | |
| Last algorithm used | /cpachecker/config/components/combinations-parallel-termination.properties | |
| Total time for algorithm 1 | 156.483s | |
| PredicateCPA statistics | ||
| Number of abstractions | 829 | 3% of all post computations |
| Times abstraction was reused | 0 | |
| Because of function entry/exit | 0 | 0% |
| Because of loop head | 800 | 97% |
| Because of join nodes | 0 | 0% |
| Because of threshold | 0 | 0% |
| Because of target state | 29 | 3% |
| Times precision was empty | 195 | 24% |
| Times precision was {false} | 18 | 2% |
| Times result was cached | 280 | 34% |
| Times cartesian abs was used | 0 | 0% |
| Times boolean abs was used | 336 | 41% |
| Times result was 'false' | 123 | 15% |
| Number of strengthen sat checks | 0 | |
| Number of coverage checks | 5947 | |
| BDD entailment checks | 628 | |
| Number of SMT sat checks | 0 | |
| trivial | 0 | |
| cached | 0 | |
| Max ABE block size | 19 | |
| Avg ABE block size | 7.72 | sum: 6402, count: 829, min: 0, max: 19 |
| Number of predicates discovered | 23 | |
| Number of abstraction locations | 5 | |
| Max number of predicates per location | 7 | |
| Avg number of predicates per location | 4 | |
| Total predicates per abstraction | 2280 | |
| Max number of predicates per abstraction | 8 | |
| Avg number of predicates per abstraction | 6.44 | |
| Number of irrelevant predicates | 594 | 26% |
| Number of preds handled by boolean abs | 1066 | 47% |
| Total number of models for allsat | 1225 | |
| Max number of models for allsat | 28 | |
| Avg number of models for allsat | 3.65 | |
| Time for post operator | 1.575s | |
| Time for path formula creation | 1.553s | |
| Time for strengthen operator | 0.043s | |
| Time for prec operator | 1.194s | |
| Time for abstraction | 1.111s | Max: 0.022s, Count: 829 |
| Boolean abstraction | 0.557s | |
| Solving time | 0.266s | Max: 0.012s |
| Model enumeration time | 0.253s | |
| Time for BDD construction | 0.065s | Max: 0.001s |
| Time for merge operator | 0.093s | |
| Time for coverage checks | 0.019s | |
| Time for BDD entailment checks | 0.012s | |
| Total time for SMT solver (w/o itp) | 0.519s | |
| Number of path formula cache hits | 18550 | 69% |
| Inside post operator | ||
| Inside path formula creation | ||
| Time for path formula computation | 1.477s | |
| Total number of created targets for pointer analysis | 0 | |
| Number of BDD nodes | 1226 | |
| Size of BDD node table | 466043 | |
| Size of BDD cache | 46619 | |
| Size of BDD node cleanup queue | 0.38 | sum: 1307, count: 3424, min: 0, max: 547 |
| Time for BDD node cleanup | 0.004s | |
| Time for BDD garbage collection | 0.000s | in 0 runs |
| KeyValue statistics | ||
| Init. function predicates | 0 | |
| Init. global predicates | 0 | |
| Init. location predicates | 0 | |
| Invariant Generation statistics | ||
| AutomatonAnalysis (NonTerminationLabelAutomaton) statistics | ||
| Number of states | 1 | |
| Total time for successor computation | 0.108s | |
| Automaton transfers with branching | 0 | |
| Automaton transfer successors | 0.97 | sum: 23125, count: 23753, min: 0, max: 1 [0 x 628, 1 x 23125] |
| Number of states with assumption transitions | 0 | |
| AutomatonAnalysis (TerminatingFunctions) statistics | ||
| Number of states | 1 | |
| Total time for successor computation | 0.029s | |
| Automaton transfers with branching | 0 | |
| Automaton transfer successors | 0.99 | sum: 23001, count: 23125, min: 0, max: 1 [0 x 124, 1 x 23001] |
| Number of states with assumption transitions | 0 | |
| Termination Algorithm statistics | ||
| Total time | 155.165s | |
| Time for recursion analysis | 0.000s | |
| Number of analysed loops | 4 | 57% |
| Total time for loop analysis | 155.160s | |
| Avg time per loop analysis | 38.790s | |
| Max time per loop analysis | 96.290s | |
| Number of safety analysis runs | 10 | |
| Avg safety analysis run per loop | 2.50 | |
| Max safety analysis run per loop | 4 for loops [N31] | |
| Total time for safety analysis | 5.564s | |
| Avg time per safety analysis run | 0.556s | |
| Max time per safety analysis run | 2.942s | |
| Number of analysed lassos | 0 | |
| Avg number of lassos per loop | 0.00 | |
| Max number of lassos per loop | 0 for loops | |
| Avg number of lassos per iteration | 0.00 | |
| Max number of lassos per iteration | 0 | |
| Total time for lassos analysis | 149.558s | |
| Avg time per iteration | 24.926s | |
| Max time per iteration | 95.029s | |
| Time for lassos construction | 149.558s | |
| Avg time for lasso construction per iteration | 24.926s | |
| Max time for lasso construction per iteration | 95.029s | |
| Time for stem and loop construction | 0.210s | |
| Avg time for stem and loop construction per iteration | 0.035s | |
| Max time for stem and loop construction per iteration | 0.111s | |
| Time for lassos creation | 149.319s | |
| Avg time for lassos creation per iteration | 24.886s | |
| Max time for lassos creation per iteration | 94.978s | |
| Total time for non-termination analysis | 0.000s | |
| Avg time for non-termination analysis per lasso | 0.000s | |
| Max time for non-termination analysis per lasso | 0.000s | |
| Total time for termination analysis | 0.000s | |
| Avg time for termination analysis per lasso | 0.000s | |
| Max time for termination analysis per lasso | 0.000s | |
| Total number of termination arguments | 0 | |
| Avg termination arguments per loop | 0.00 | |
| Max termination arguments per loop | 0 for loops | |
| Counterexample-Check Algorithm statistics | ||
| Number of counterexample checks | 0 | |
| Termination Algorithm statistics | ||
| Total time | 155.165s | |
| Time for recursion analysis | 0.000s | |
| Number of analysed loops | 4 | 57% |
| Total time for loop analysis | 155.160s | |
| Avg time per loop analysis | 38.790s | |
| Max time per loop analysis | 96.290s | |
| Number of safety analysis runs | 10 | |
| Avg safety analysis run per loop | 2.50 | |
| Max safety analysis run per loop | 4 for loops [N31] | |
| Total time for safety analysis | 5.564s | |
| Avg time per safety analysis run | 0.556s | |
| Max time per safety analysis run | 2.942s | |
| Number of analysed lassos | 0 | |
| Avg number of lassos per loop | 0.00 | |
| Max number of lassos per loop | 0 for loops | |
| Avg number of lassos per iteration | 0.00 | |
| Max number of lassos per iteration | 0 | |
| Total time for lassos analysis | 149.558s | |
| Avg time per iteration | 24.926s | |
| Max time per iteration | 95.029s | |
| Time for lassos construction | 149.558s | |
| Avg time for lasso construction per iteration | 24.926s | |
| Max time for lasso construction per iteration | 95.029s | |
| Time for stem and loop construction | 0.210s | |
| Avg time for stem and loop construction per iteration | 0.035s | |
| Max time for stem and loop construction per iteration | 0.111s | |
| Time for lassos creation | 149.319s | |
| Avg time for lassos creation per iteration | 24.886s | |
| Max time for lassos creation per iteration | 94.978s | |
| Total time for non-termination analysis | 0.000s | |
| Avg time for non-termination analysis per lasso | 0.000s | |
| Max time for non-termination analysis per lasso | 0.000s | |
| Total time for termination analysis | 0.000s | |
| Avg time for termination analysis per lasso | 0.000s | |
| Max time for termination analysis per lasso | 0.000s | |
| Total number of termination arguments | 0 | |
| Avg termination arguments per loop | 0.00 | |
| Max termination arguments per loop | 0 for loops | |
| Counterexample-Check Algorithm statistics | ||
| Number of counterexample checks | 0 | |
| Code Coverage | ||
| Function coverage | 0.857 | |
| Visited lines | 321 | |
| Total lines | 336 | |
| Line coverage | 0.955 | |
| Visited conditions | 44 | |
| Total conditions | 56 | |
| Condition coverage | 0.786 | |
| CPAchecker general statistics | ||
| Number of program locations | 440 | |
| Number of CFA edges (per node) | 448 | count: 440, min: 0, max: 2, avg: 1.02 |
| Number of relevant variables | 19 | |
| Number of functions | 7 | |
| Number of loops (and loop nodes) | 7 | sum: 76, min: 3, max: 27, avg: 10.86 |
| Size of reached set | 573 | |
| Number of reached locations | 89 | 20% |
| Avg states per location | 6 | |
| Max states per location | 35 | at node N1 |
| Number of reached functions | 6 | 86% |
| Number of partitions | 89 | |
| Avg size of partitions | 6 | |
| Max size of partitions | 35 | with key N1 |
| Number of target states | 1 | |
| Size of final wait list | 11 | |
| Time for analysis setup | 1.447s | |
| Time for loading CPAs | 0.020s | |
| Time for loading parser | 0.210s | |
| Time for CFA construction | 1.171s | |
| Time for parsing file(s) | 0.414s | |
| Time for AST to CFA | 0.366s | |
| Time for CFA sanity check | 0.061s | |
| Time for post-processing | 0.197s | |
| Time for loop structure | 0.012s | |
| Time for AST structure | 0.000s | |
| Time for CFA export | 0.681s | |
| Time for function pointers resolving | 0.004s | |
| Function calls via function pointers | 0 | count: 1, min: 0, max: 0, avg: 0.00 |
| Instrumented function pointer calls | 0 | count: 1, min: 0, max: 0, avg: 0.00 |
| Function calls with function pointer arguments | 0 | count: 1, min: 0, max: 0, avg: 0.00 |
| Instrumented function pointer arguments | 0 | count: 1, min: 0, max: 0, avg: 0.00 |
| Time for classifying variables | 0.095s | |
| Time for collecting variables | 0.056s | |
| Time for solving dependencies | 0.004s | |
| Time for building hierarchy | 0.000s | |
| Time for building classification | 0.029s | |
| Time for exporting data | 0.006s | |
| Time for Analysis | 156.484s | |
| CPU time for analysis | 189.300s | |
| Total time for CPAchecker | 157.943s | |
| Total CPU time for CPAchecker | 191.820s | |
| Time for statistics | 0.189s | |
| Time for Garbage Collector | 2.013s | in 1934 runs |
| Garbage Collector(s) used | PS MarkSweep, PS Scavenge | |
| Used heap memory | 206MB ( 196 MiB) max; 108MB ( 103 MiB) avg; 219MB ( 209 MiB) peak | |
| Used non-heap memory | 68MB ( 65 MiB) max; 65MB ( 62 MiB) avg; 70MB ( 66 MiB) peak | |
| Used in PS Old Gen pool | 122MB ( 116 MiB) max; 69MB ( 66 MiB) avg; 122MB ( 116 MiB) peak | |
| Allocated heap memory | 263MB ( 251 MiB) max; 260MB ( 248 MiB) avg | |
| Allocated non-heap memory | 71MB ( 68 MiB) max; 69MB ( 66 MiB) avg | |
| Total process virtual memory | 14982MB ( 14288 MiB) max; 14964MB ( 14271 MiB) avg |
| # | Configuration Name | Configuration Value |
|---|---|---|
| 1 | analysis.algorithm.termination | true |
| 2 | analysis.machineModel | Linux64 |
| 3 | analysis.name | terminationAnalysis |
| 4 | analysis.programNames | Benchmarks/TermCOMP/C/SV-COMP_Mixed_Categories/merge_sort_true-unreach-call/merge_sort_true-unreach-call.c |
| 5 | analysis.restartAfterUnknown | true |
| 6 | counterexample.export.exportWitness | false |
| 7 | cpa.arg.lateMerge | prevent |
| 8 | language | C |
| 9 | log.level | INFO |
| 10 | parser.usePreprocessor | true |
| 11 | restartAlgorithm.configFiles | components/combinations-parallel-termination.properties, components/termination-recursion.properties::if-recursive |
| 12 | specification | |
| 13 | statistics.print | true |
| 14 | termination.config | terminationAnalysis.properties |
This table was generated by CPAchecker. For feedback, questions, and bug reports please use our issue tracker.
License: Apache 2.0 License
Source: {{dependency.repository}}
{{dependency.copyright}}
License:
Full text of license
{{dependencies.licenses[dependency.licenseId]}}